perm filename PROVER.NOT[1,JRA] blob sn#033001 filedate 1973-04-03 generic text, type T, neo UTF8
00100	THE RITUAL FOR CONSTRUCTION THE PROVER IS COMPLICATED BY THE 
00200	USE OF A SYNTAX DIRECTED I/O (SDIO)PACKAGE FOR THE PARSERS.
00300	THE RESULTING FLEXIBILITY AS PROVED TO BE WORTH THE EXTRA HASSLE.
00400	
00500	FILES:
00600	PROVE1.NEW 	LISP VERSION OF THE PROVER. THIS SHOULD BE COMPILED
00700			WITH FILE  NAMED SPECIA.
00800			R COMPLR...(DSKIN SPECIA)...(COMPL(PROVE1.NEW))
00900	
00950	MATCHE.NEW	THE SEMANTIC ROUTINES FOR THE MATCHER
01000	
01100	PROVER.PRM	PRIMITIVE LAP ROUTINES
01200	
01300	SDIO		LISP PRIMITIVES FOR SDIO PACKAGE.
01400	
01500	SCAN &PRIM	MACHINE LANG PRIMITIVES FOR SDIO
01600	
01700	UNIF		MACHINE LANGUAGE PRIMITIVES FOR PROVER.
01800	
01900	STATEV		INITIALIZATION H.S.
02000	
02100	COMMAND & EDIT & INFIX & MATCH.LSP
02200			THESE ARE THE LISP FILES FOR THE SDIO PACKAGE
02300			IF YOU WANT THE DOCUMENTATION FOR SDIO AND THE
02400			FILES WHICH GENERATE THE PARSERS THEY CAN BE SPPLIED.
02500	
02600	FIX.LSP		SDIO ISN'T PERFECT. THESE FILES MAKE IT SO.
02700	SDIOMA		MACROS NECESSARY FOR COMPILATION OF ANY OF THE SDIO
02800			FILES.
02900	
03000	TO BUILD THE PROVER:
03100	THE PROVER CAN BE CREATED IN 37K.USING 2000 FULL WORDS AND 36000 BPS.
03200	THIS IS AN EXTRA LARGE PORTION OF BPS BUT IS USEFUL FOR PATCHING WITHOUT
03300	RECOMPILING THE WHOLE SYSTEM.
03400	THE ORDER OF LOADING SHOULD BE:
03500	PROVE1.LAP,MATCHER.LAP,SDIO.LAP,SCAN.REL,PRIM.REL,UNIF.REL,STATEV.NEW,PROVER.PRM
03550	NOTE: THE REL FILES SHOULD BE ENTERED VIA "(LOAD T)".
03600	AT THIS POINT (PRINIT)MAY BE EXECUTED.
03700	NOW THE SDIO: COMMAND.LAP,EDIT.LAP,MATCH.LAP,INFIX.LAP,FIX.LAP
03800	(FIX.LAP SHOUL COME LAST).